(DEFPROP LANG 
 (NIL LANG
      ISITM
      ISITNM
      MAKVAR
      PREPREDLET
      INFPREDLET
      INFN
      PREFN
      VARNO
      VARTBL
      <PREPREDLET>
      <INFPREDLET>
      <PREFN>
      <INFN>
      <IVAR>
      >PREPREDLET<
      >INFPREDLET<
      >PREFN<
      >INFN<
      >IVAR<) 
VALUE)

(DEFPROP ISITM 
 (LAMBDA(L)
  (LIST (QUOTE FUNCTION)
	(LIST (QUOTE LAMBDA)
 	      NIL
	      (LIST (QUOTE PROG)
		    (QUOTE (Z))
		    (LIST (QUOTE RETURN)
			  (LIST (QUOTE COND)
				(LIST (LIST (QUOTE SETQ) (QUOTE Z) (LIST (QUOTE ISIT) (CADR L))) (QUOTE Z))
				(QUOTE (*NIL*)))))))) 
MACRO)

(DEFPROP ISITNM 
 (LAMBDA(L)
  (LIST (QUOTE FUNCTION)
	(LIST (QUOTE LAMBDA)
 	      NIL
	      (LIST (QUOTE PROG)
		    (QUOTE (Z))
		    (LIST (QUOTE RETURN)
			  (LIST (QUOTE COND)
				(LIST (LIST (QUOTE SETQ) (QUOTE Z) (LIST (QUOTE ISITN) (CADR L))) (QUOTE Z))
				(QUOTE (*NIL*)))))))) 
MACRO)

(DEFPROP MAKVAR 
 (LAMBDA(X)
  (PROG (Z)
	(SETQ Z (ASSOC X VARTBL))
	(COND (Z (RETURN (CDR Z))))
	(SETQ VARTBL (CONS (CONS X (SETQ VARNO (ADD1 VARNO))) VARTBL))
	(RETURN VARNO))) 
EXPR)

(DEFPROP PREPREDLET 
 (NIL P Q R E) 
VALUE)

(DEFPROP INFPREDLET 
 (NIL ε < = ≤) 
VALUE)

(DEFPROP INFN 
 (NIL ⊗ //) 
VALUE)

(DEFPROP PREFN 
 (NIL 0 1 A B C F) 
VALUE)

(DEFPROP VARNO 
 (NIL . 0) 
VALUE)

(DEFPROP <PREPREDLET> 
 (LAMBDA NIL (NLRR (QUOTE PREPREDLET) (ISITM PREPREDLET))) 
EXPR)

(DEFPROP <INFPREDLET> 
 (LAMBDA NIL (NLRR (QUOTE INFPREDLET) (ISITM INFPREDLET))) 
EXPR)

(DE <PREDLET>()(NLRR @PREDLET (ISITM (APPEND INFPREDLET PREPREDLET))))

(DE <FNLET>()(NLRR @FJLET (ISITM(APPEND INFN PREFN))))

(DE <OP>()(NLRR @OP (ISITNM CONNECT)))

(DE <DECOP>()(NLRR @DECOP (ISITM DECOP)))

(DE <AXIOMNAME>()(NLRR @AXIOMNAME(ISITM AXIOMLST)))

(DEFPROP <PREFN> 
 (LAMBDA NIL (NLRR (QUOTE PREFN) (ISITM PREFN))) 
EXPR)

(DEFPROP <INFN> 
 (LAMBDA NIL (NLRR (QUOTE INFN) (ISITM INFN))) 
EXPR)

(DEFPROP <IVAR> 
 (LAMBDA NIL
  (NLRR (QUOTE IVAR)
	(FUNCTION (LAMBDA NIL (PROG (Z) (RETURN (COND ((SETQ Z (ISIT IVAR)) (MAKVAR Z)) (*NIL*)))))))) 
EXPR)

(DEFPROP >PREPREDLET< 
 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) PREPREDLET) (STK1))))))) 
EXPR)

(DEFPROP >INFPREDLET< 
 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) INFPREDLET) (STK1))))))) 
EXPR)

(DEFPROP >PREFN< 
 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) PREFN) (STK1))))))) 
EXPR)

(DEFPROP >INFN< 
 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) INFN) (STK1))))))) 
EXPR)

(DE >DECOP< (%N)(OUTRUL %N(FUNCTION(LAMBDA NIL(COND((MEMQ(STK1) DECOP)(STK1)))))))

(DEFPROP >IVAR< 
 (LAMBDA(%N)
  (OUTRUL %N
	  (FUNCTION
	   (LAMBDA NIL
	    (COND ((NUMBERP (STK1)) (CDR (ASSOC (STK1) OUTVAR)))
		  ((EQ (STK1) (QUOTE LENGTH)) LENGTH)
		  ((EQ (STK1) (QUOTE DEPTH)) DEPTH)))))) 
EXPR)



(DEFPROP >TM< 
 (LAMBDA(%N)
  (OUTRUL %N
	  (FUNCTION
	   (LAMBDA NIL
	    (COND ((>IVAR< 1) (STK1))
		  ((AND (MATCH (QUOTE (*))) (>PREFN< 0)) (STK0))
		  ((AND (MATCH (QUOTE (* * *))) (>INFN< 2) (>TM< 1) (>TM1< 0))
		   (LIST (QUOTE (:CH /()) (STK1) (STK2) (STK0) (QUOTE (:CH /)))))
		  ((AND (MATCH (QUOTE (* . *))) (>PREFN< 1) (>ITMLST< 0)) (LIST (STK1) (STK0)))
		  ((>TM< 1) (LIST (QUOTE (:CH /()) (STK1) (QUOTE (:CH /)))))))))) 
EXPR)



(DEFPROP >AND1< 
 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((EQ (QUOTE AND) (STK1)) (QUOTE (:CH ∧)))))))) 
EXPR)

(DEFPROP >OR1< 
 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((EQ (QUOTE OR) (STK1)) (QUOTE (:CH ∨)))))))) 
EXPR)

(DEFPROP >NOT1< 
 (LAMBDA (%N) (OUTRUL %N (FUNCTION (LAMBDA NIL (COND ((EQ (QUOTE NOT) (STK1)) (QUOTE (:CH ¬)))))))) 
EXPR)
(DE >EQUIV1< (%N)(OUTRUL %N(FUNCTION(LAMBDA NIL(COND((EQ @EQUIV (STK1)) @(:CH ≡))))))) 
(DE >IMP1<  (%N)(OUTRUL %N(FUNCTION(LAMBDA NIL(COND((EQ @IMP (STK1)) @(:CH ⊃))))))) 
(DEFPROP >QFF< 
 (LAMBDA(%N)
  (OUTRUL %N
	  (FUNCTION
	   (LAMBDA NIL
	    (COND ((EQ (QUOTE FA) (STK1)) (QUOTE (:CH ∀))) ((EQ (QUOTE TE) (STK1)) (QUOTE (:CH ∃)))))))) 
EXPR)





(DEFPROP GET1 
 (LAMBDA (X L) (COND ((NUMBERP X) NIL) (T (GET X L)))) 
EXPR)

(DEFPROP SPACING 
 (LAMBDA(OLD NEW)
  (PROG2 (SETQ LAST NEW)
	 (CDR (SASSOC NEW (GET1 OLD (QUOTE SPACING)) (FUNCTION (LAMBDA NIL (QUOTE (NIL . 0)))))))) 
EXPR)

(DEFPROP CONNECT 
 (NIL ; /) /( /. /, ≡ ⊃ → ↔ ∨ ∧ ∀ ∃ ¬ &) 
VALUE)

(DEFPROP RESERVEDWORDS 
 (NIL IMP EQUIV  AND NOT OR FA TE) 
VALUE)



(DEFPROP DOPRINT 
 (LAMBDA(L)
  (COND ((ATOM L) (SPACES LAST (QUOTE >ATOM<)) (PRINC L))
	((EQ (CAR L) (QUOTE :CH)) (SPACES LAST (CADR L)) (PRINC (CADR L)))
	((EQ (CAR L) (QUOTE %IN)))
	(T (MAPC (FUNCTION DOPRINT) (CDR L))))) 
EXPR)


(DEFPROP DECTBL 
 (NIL (PRE_OP . PREFN)
      (EQUALITY . EQUAL)
      (PRE_PRED . PREPREDLET)
      (INF_OP . INFN)
      (INF_PRED . INFPREDLET)
      (VAR . IVAR)) 
VALUE)

(DEFPROP DECOP 
 (NIL EQUALITY VAR INF_PRED INF_OP PRE_PRED PRE_OP) 
VALUE)

(DE OUTIT(XYZ)(PROG(STFLG)(SETQ STFLG T)(OUT >ST< XYZ)))
(DEFPROP >OP< 
 (LAMBDA (X) (OUTRUL X (FUNCTION (LAMBDA NIL (COND ((MEMQ (STK1) CONNECT) NIL) (T (STK1))))))) 
EXPR)